Problem:
 c(c(c(y))) -> c(c(a(y,0())))
 c(a(a(0(),x),y)) -> a(c(c(c(0()))),y)
 c(y) -> y

Proof:
 Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {3}
   transitions:
    a1(11,2) -> 3*
    a1(11,1) -> 3*
    c1(10) -> 11*
    c1(9) -> 10*
    c1(8) -> 9*
    01() -> 8*
    c2(17) -> 11*
    c2(16) -> 17*
    c0(2) -> 3*
    c0(1) -> 3*
    a2(8,15) -> 16*
    a0(1,2) -> 1*
    a0(2,1) -> 1*
    a0(1,1) -> 1*
    a0(2,2) -> 1*
    02() -> 15*
    00() -> 2*
    1 -> 3*
    2 -> 3*
    8 -> 9*
    9 -> 10*
    10 -> 11*
    16 -> 17*
    17 -> 11*
  problem:
   
  Qed